$\forall$${\it es}$:ES, $e$, $a$:E. ($a$ $<$loc $e$) $\Rightarrow$ ($\exists$$b$:E. $\neg$first($b$) \& $a$ $=$ pred($b$) \& $b$ $\leq$ $e$ )